$\forall$$T$:Type, $x$:$T$, $l$:($T$ List), $i$:int\_seg(0; $\parallel$$l$$\parallel$). sqequal(cons($x$; $l$)[($i$ + 1)]; $l$[$i$])